@i (with ds: ds init: init action a:T precondition a(v) is P s v)(j)
== if eqof(IdDeq)(j,i) with ds: ds init: initaction a:T precondition a(v) is P else  fi 

latex

Definitions	x.A(x), if b t else f fi, f(a), eqof(d), IdDeq, with ds: ds init: initaction a:T precondition a(v) is P,
FDL editor aliases	d-single-pre-init